$\forall$${\it es}$:ES, $i$:Id, ${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type.
\\[0ex]${\it ds}_{2}$ $\subseteq$ ${\it ds}_{1}$ $\Rightarrow$ ($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}_{1}$($x$)?Top) $\Rightarrow$ state@$i$ $\subseteq\rho$ State(${\it ds}_{2}$)